(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 47) (_ BitVec 70)) (_ BitVec 40))
(declare-fun p0 ( (_ BitVec 123) (_ BitVec 8) (_ BitVec 82)) Bool)
(declare-fun p1 ( (_ BitVec 20)) Bool)
(declare-fun v0 () (_ BitVec 91))
(declare-fun v1 () (_ BitVec 68))
(declare-fun v2 () (_ BitVec 100))
(assert (let ((e3(_ bv83312496745967668830250057391 97)))
(let ((e4(_ bv2675021346179795940312842572916 102)))
(let ((e5 (f0 ((_ extract 50 4) v0) ((_ extract 92 23) v2))))
(let ((e6 (ite (p1 ((_ extract 99 80) e4)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (ite (p0 ((_ zero_extend 122) e6) ((_ extract 29 22) e5) ((_ sign_extend 42) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvsrem e3 e3)))
(let ((e9 (bvsub e5 ((_ zero_extend 39) e6))))
(let ((e10 (ite (p0 ((_ sign_extend 83) e5) ((_ sign_extend 7) e7) ((_ zero_extend 42) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e11 (bvnand ((_ zero_extend 96) e6) e3)))
(let ((e12 (bvsub ((_ zero_extend 5) e11) e4)))
(let ((e13 (ite (bvule v0 ((_ sign_extend 51) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e14 (bvsrem ((_ zero_extend 39) e7) e9)))
(let ((e15 (ite (bvult v2 ((_ zero_extend 3) e11)) (_ bv1 1) (_ bv0 1))))
(let ((e16 (bvand v1 ((_ zero_extend 67) e10))))
(let ((e17 (p1 ((_ sign_extend 19) e10))))
(let ((e18 (bvugt ((_ zero_extend 39) e7) e9)))
(let ((e19 (p0 ((_ sign_extend 83) e9) ((_ zero_extend 7) e15) ((_ sign_extend 81) e13))))
(let ((e20 (distinct e3 e11)))
(let ((e21 (distinct ((_ zero_extend 11) v0) e12)))
(let ((e22 (bvsgt ((_ zero_extend 101) e10) e12)))
(let ((e23 (bvule e9 ((_ zero_extend 39) e13))))
(let ((e24 (bvult ((_ sign_extend 62) e14) e4)))
(let ((e25 (bvuge v0 ((_ zero_extend 23) v1))))
(let ((e26 (bvule e12 ((_ zero_extend 101) e6))))
(let ((e27 (p0 ((_ zero_extend 21) e12) ((_ extract 18 11) e9) ((_ zero_extend 81) e13))))
(let ((e28 (bvult ((_ zero_extend 101) e7) e12)))
(let ((e29 (bvsgt e4 ((_ sign_extend 62) e5))))
(let ((e30 (bvslt ((_ zero_extend 39) e15) e9)))
(let ((e31 (p0 ((_ zero_extend 26) e8) ((_ extract 94 87) e11) ((_ zero_extend 42) e14))))
(let ((e32 (bvsle ((_ zero_extend 57) e9) e8)))
(let ((e33 (bvslt ((_ zero_extend 28) e5) e16)))
(let ((e34 (bvsge e4 e12)))
(let ((e35 (bvult e4 ((_ zero_extend 101) e13))))
(let ((e36 (bvsge ((_ sign_extend 67) e6) v1)))
(let ((e37 (bvslt e16 ((_ sign_extend 28) e9))))
(let ((e38 (bvugt e15 e13)))
(let ((e39 (bvugt e5 ((_ zero_extend 39) e13))))
(let ((e40 (distinct v1 ((_ sign_extend 67) e6))))
(let ((e41 (= ((_ sign_extend 67) e6) v1)))
(let ((e42 (= v2 ((_ zero_extend 99) e13))))
(let ((e43 (=> e17 e34)))
(let ((e44 (and e28 e29)))
(let ((e45 (= e27 e30)))
(let ((e46 (and e22 e23)))
(let ((e47 (and e42 e20)))
(let ((e48 (=> e43 e36)))
(let ((e49 (=> e24 e19)))
(let ((e50 (=> e31 e47)))
(let ((e51 (or e18 e33)))
(let ((e52 (or e46 e40)))
(let ((e53 (= e35 e52)))
(let ((e54 (= e44 e51)))
(let ((e55 (=> e45 e39)))
(let ((e56 (or e54 e50)))
(let ((e57 (or e25 e38)))
(let ((e58 (and e26 e49)))
(let ((e59 (=> e53 e58)))
(let ((e60 (xor e37 e48)))
(let ((e61 (= e57 e57)))
(let ((e62 (and e59 e59)))
(let ((e63 (not e32)))
(let ((e64 (not e60)))
(let ((e65 (= e61 e64)))
(let ((e66 (=> e21 e65)))
(let ((e67 (not e66)))
(let ((e68 (ite e67 e56 e41)))
(let ((e69 (not e63)))
(let ((e70 (not e68)))
(let ((e71 (or e55 e70)))
(let ((e72 (= e62 e62)))
(let ((e73 (or e69 e72)))
(let ((e74 (xor e71 e73)))
(let ((e75 (and e74 (not (= e3 (_ bv0 97))))))
(let ((e76 (and e75 (not (= e3 (bvnot (_ bv0 97)))))))
(let ((e77 (and e76 (not (= e9 (_ bv0 40))))))
(let ((e78 (and e77 (not (= e9 (bvnot (_ bv0 40)))))))
e78
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
